(0) Obligation:
Clauses:
m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
=(X, X).
Query: q(g,g,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
user_defined_=(X, X).
Query: q(g,g,a)
(3) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(4) Obligation:
Triples:
mA(s(X1), s(X2), X3) :- mA(X1, X2, X3).
qB(s(X1), s(X2), X3) :- mA(X1, X2, X3).
Clauses:
mcA(X1, 0, X1).
mcA(0, X1, 0).
mcA(s(X1), s(X2), X3) :- mcA(X1, X2, X3).
Afs:
qB(x1, x2, x3) = qB(x1, x2)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
qB_in: (b,b,f)
mA_in: (b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
QB_IN_GGA(s(X1), s(X2), X3) → U2_GGA(X1, X2, X3, mA_in_gga(X1, X2, X3))
QB_IN_GGA(s(X1), s(X2), X3) → MA_IN_GGA(X1, X2, X3)
MA_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, mA_in_gga(X1, X2, X3))
MA_IN_GGA(s(X1), s(X2), X3) → MA_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
mA_in_gga(
x1,
x2,
x3) =
mA_in_gga(
x1,
x2)
QB_IN_GGA(
x1,
x2,
x3) =
QB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
MA_IN_GGA(
x1,
x2,
x3) =
MA_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QB_IN_GGA(s(X1), s(X2), X3) → U2_GGA(X1, X2, X3, mA_in_gga(X1, X2, X3))
QB_IN_GGA(s(X1), s(X2), X3) → MA_IN_GGA(X1, X2, X3)
MA_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, mA_in_gga(X1, X2, X3))
MA_IN_GGA(s(X1), s(X2), X3) → MA_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
mA_in_gga(
x1,
x2,
x3) =
mA_in_gga(
x1,
x2)
QB_IN_GGA(
x1,
x2,
x3) =
QB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
MA_IN_GGA(
x1,
x2,
x3) =
MA_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MA_IN_GGA(s(X1), s(X2), X3) → MA_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
MA_IN_GGA(
x1,
x2,
x3) =
MA_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(9) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MA_IN_GGA(s(X1), s(X2)) → MA_IN_GGA(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(11) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MA_IN_GGA(s(X1), s(X2)) → MA_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(12) YES